ds:x:Id fp Type, da:k:Knd fp Type, v:ecl-trans-tuple{i:l}(ds;da), L:event-info(ds;da) List,
x:1of(v).
ecl-trans-reachable(ds;da;v;L;x)  Prop 

latex

Definitions	t  T, Valtype(da;k), KindDeq, Knd, x:A. B(x), (x  l), b, Prop, A, b, , deq-member(eq;x;L), P  Q, P & Q, P  Q, Unit, event-info(ds;da), State(ds), Top, f(x)?z, if b t else f fi, x,y. t(x;y), list_accum(x,a.f(x;a);y;l), ||as||, l1  l2, A & B, x:A. B(x), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-reachable(ds;da;v;L;x), ecl-trans-tuple{i:l}(ds;da), 1of(t), x. t(x), a:A fp B(a), Id
Lemmas	Id wf, fpf wf, ecl-trans-tuple wf, iseg wf, length wf1, list accum wf, ifthenelse wf, event-info wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, l member wf, Knd wf, Kind-deq wf